SherbyNet - /page/wikibook/entry.mu

Micron Document

`:top

`!Refinement`! is a generic term of computer science that encompasses various approaches for producing `F33f`_`[correct`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Correctness_(computer_science)]`_`f computer programs and simplifying existing programs to enable their formal verification.

>>Contents

• `F0af`_`[Program refinement`#program-refinement]`_`f

• `F0af`_`[Data refinement`#data-refinement]`_`f

• `F0af`_`[Refinement calculus`#refinement-calculus]`_`f

• `F0af`_`[Refinement types`#refinement-types]`_`f

• `F0af`_`[See also`#see-also]`_`f

• `F0af`_`[References`#references]`_`f

-─

>>Program refinement

In `F33f`_`[formal methods`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Formal_methods]`_`f, `!program refinement`! is the `F33f`_`[verifiable`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Formal_verification]`_`f transformation of an `*abstract`* (high-level) `F33f`_`[formal specification`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Formal_specification]`_`f into a `*concrete`* (low-level) `F33f`_`[executable program`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Executable_program]`_`f. `*`F33f`_`[Stepwise refinement`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Stepwise_refinement]`_`f`* allows this process to be done in stages. Logically, refinement normally involves `F33f`_`[implication`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Logical_consequence]`_`f, but there can be additional complications.

The progressive just-in-time preparation of the product backlog (requirements list) in `F33f`_`[agile software development`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Agile_software_development]`_`f approaches, such as `F33f`_`[Scrum`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Scrum_(software_development)]`_`f, is also commonly described as refinement.`:cite-ref-1[`F5bf`_`[1`#cite-note-1]`_`f]

>>Data refinement

`!Data refinement`! is used to convert an abstract data model (in terms of `F33f`_`[sets`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Set_(mathematics)]`_`f for example) into implementable `F33f`_`[data structures`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Data_structures]`_`f (such as `F33f`_`[arrays`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Array_data_structure]`_`f). Operation refinement converts a `F33f`_`[specification`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Specification]`_`f of an operation on a system into an implementable `F33f`_`[program`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Computer_program]`_`f (e.g., a `F33f`_`[procedure`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Procedure_(computer_science)]`_`f). The `F33f`_`[postcondition`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Postcondition]`_`f can be strengthened and/or the `F33f`_`[precondition`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Precondition]`_`f weakened in this process. This reduces any `F33f`_`[nondeterminism`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Nondeterministic_algorithm]`_`f in the specification, typically to a completely `F33f`_`[deterministic`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Deterministic]`_`f implementation.

For example, `*x`* ∈ {1,2,3} (where `*x`* is the value of the `F33f`_`[variable`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Variable_(programming)]`_`f `*x`* after an operation) could be refined to `*x`* ∈ {1,2}, then `*x`* ∈ {1}, and implemented as `*x`* := 1. Implementations of `*x`* := 2 and `*x`* := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine to `*x`* ∈ {} (equivalent to `*false`*) since this is unimplementable; it is impossible to select a `F33f`_`[member`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Element_(mathematics)]`_`f from the `F33f`_`[empty set`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Empty_set]`_`f.

The term `F33f`_`[reification`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Reification_(computer_science)]`_`f is also sometimes used (coined by `F33f`_`[Cliff Jones`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Cliff_Jones_(computer_scientist)]`_`f). `F33f`_`[Retrenchment`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Retrenchment_(computing)]`_`f is an alternative technique when formal refinement is not possible. The opposite of refinement is `F33f`_`[abstraction`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Abstraction_(computer_science)]`_`f.

>>Refinement calculus

`F33f`_`[Refinement calculus`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Refinement_calculus]`_`f is a `F33f`_`[formal system`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Formal_system]`_`f (inspired from `F33f`_`[Hoare logic`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Hoare_logic]`_`f) that promotes program refinement. The FermaT Transformation System is an industrial-strength implementation of refinement. The `F33f`_`[B-Method`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=B-Method]`_`f is also a `F33f`_`[formal method`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Formal_method]`_`f that extends refinement calculus with a component language: it has been used in industrial developments.

>>Refinement types

In `F33f`_`[type theory`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Type_theory]`_`f, a `!refinement type`!`:cite-ref-2[`F5bf`_`[2`#cite-note-2]`_`f]`:cite-ref-3[`F5bf`_`[3`#cite-note-3]`_`f]`:cite-ref-4[`F5bf`_`[4`#cite-note-4]`_`f] is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express `F33f`_`[preconditions`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Precondition]`_`f when used as `F33f`_`[function arguments`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Function_argument]`_`f or `F33f`_`[postconditions`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Postcondition]`_`f when used as `F33f`_`[return types`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Return_type]`_`f: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as f : N → → { n : N | n > 5 } {\\displaystyle f:\\mathbb {N} \\rightarrow \\{n:\\mathbb {N} \\,|\\,n>5\\}} . Refinement types are thus related to `F33f`_`[behavioral subtyping`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Behavioral_subtyping]`_`f.

>>See also

• `F33f`_`[Reification (computer science)`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Reification_(computer_science)]`_`f

>>References

`:cite-note-1`!1.`! `F0af`_`[↑`#cite-ref-1]`_`f `:citerefcho2009`aCho, L (2009). "Adopting an Agile Culture a User Experience Team's Journey". `*2009 Agile Conference`*. pp. 416–421. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1109/AGILE.2009.76. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-0-7695-3768-9. `F33f`_`[S2CID`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=S2CID_(identifier)]`_`f 38580329.

`:cite-note-2`!2.`! `F0af`_`[↑`#cite-ref-2]`_`f `:citereffreemanpfenning1991`aFreeman, T.; Pfenning, F. (1991). "Refinement types for ML" (PDF). `*Proceedings of the ACM Conference on Programming Language Design and Implementation`*. pp. 268–277. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1145/113445.113468.

`:cite-note-3`!3.`! `F0af`_`[↑`#cite-ref-3]`_`f `:citerefhayashi1993`aHayashi, S. (1993). "Logic of refinement types". `*Proceedings of the Workshop on Types for Proofs and Programs`*. pp. 157–172. `F33f`_`[CiteSeerX`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=CiteSeerX_(identifier)]`_`f 10.1.1.38.6346. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/3-540-58085-9_74.

`:cite-note-4`!4.`! `F0af`_`[↑`#cite-ref-4]`_`f `:citerefdenney1998`aDenney, E. (1998). "Refinement types for specification". `*Proceedings of the IFIP International Conference on Programming Concepts and Methods`*. Vol. 125. Chapman & Hall. pp. 148–166. `F33f`_`[CiteSeerX`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=CiteSeerX_(identifier)]`_`f 10.1.1.22.4988.

`c`F0af`_`[↑ Back to top`#top]`_`f`a